/*
 * $Id: JPFStaticChecker.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 * 
 */
package org.objectweb.fractal.bpc.checker;

import java.io.IOException;
import java.io.OutputStream;
import java.io.PrintStream;
import java.util.Set;
import java.util.HashSet;

import org.objectweb.fractal.bpc.checker.DFSR.JPFCooperatingTraverser;
import org.objectweb.fractal.bpc.checker.DFSR.JPFTraverser;
import org.objectweb.fractal.bpc.checker.node.ActionRepository;
import org.objectweb.fractal.bpc.checker.node.DeterministicNode;
import org.objectweb.fractal.bpc.checker.node.EventNode;
import org.objectweb.fractal.bpc.checker.node.TreeNode;
import org.objectweb.fractal.bpc.checker.parser.Builder;
import org.objectweb.fractal.bpc.checker.parser.StringTokenizer;
import org.objectweb.fractal.bpc.checker.parser.SyntaxErrorException;
import org.objectweb.fractal.bpc.checker.state.Signature;

public class JPFStaticChecker {
    
    /**
     * Creates a new instance of JPFStaticChecker.
     * @param protocol the frame protocol of the component
     * @throws SyntaxErrorException if there is a syntax error within the input protocol
     */
    public JPFStaticChecker(String protocol, boolean cooperating, PrintStream output) throws SyntaxErrorException {
        ActionRepository repository = new ActionRepository();
        rootNode = new DeterministicNode(new Builder(repository).build(new StringTokenizer(protocol), true));
        
        if (rootNode != null)
              Signature.setSize(rootNode.getLeafCount());
        
        if (cooperating)
            notifee = new JPFCooperatingTraverser(rootNode, repository, output);
        else
            notifee = new JPFTraverser(rootNode, repository, output);
        
    }
    
    /**
     * @return an instance of the JPFTraverser class, which is used as a notifee from the ProtocolListener.
     */
    public JPFTraverser getNotifee() {
        return notifee;
    }
    
    /**
     * @return list of names of events that are mentioned in the protocol (e.g. for the protocol "?i.a^;!j.b$" returns "i.a,j.b").
     */
    public static String[] getEvents(String protoStr) throws Exception
    {
		StringTokenizer st = new StringTokenizer(protoStr);
		ActionRepository ar = new ActionRepository();
		Builder b = new Builder(ar);

		TreeNode protoNode = b.build(st, false);
		
        Set eventNames = new HashSet();
       
        extractEventNames(protoNode, eventNames);

        return (String[]) eventNames.toArray(new String[eventNames.size()]);
	}
    
    public boolean wantsBacktrack() {
        return notifee.wantsBacktrack();
    }
    
    private static void extractEventNames(TreeNode tn, Set eventNames)
    {
        if (tn instanceof EventNode) 
        {
            eventNames.add( tn.protocol.substring(1, tn.protocol.length()-1) );
            return;
        }
        
        TreeNode[] children = tn.getChildren();
        
        for (int i = 0; i < children.length; i++)
        {
            extractEventNames(children[i], eventNames);
        }
    }
    
    /**
     * Writes a html file with protocol usage 
     * @param out the output stream to write to 
     * @throws IOException in case of an error when writing to the stream
     */
    public void writeUsageFile(OutputStream out) throws IOException {
        notifee.writeUsageFile(out);
    }

    
    
    private JPFTraverser notifee;

    private TreeNode rootNode;

}
